What can we do (technically) to get “the right specification”?

One can use formal approaches either post facto to try to show that a program has desirable properties (main of which is that it satisfies a specification); or one can go for correctness by construction. I not only prefer the latter but I have also argued that this is the main way to get formal methods to pay off: there is more mileage in getting a clean architecture than in trying to debug a bad design by retrofitting a proof; I thing this is also a way to choose an appropriate level of formality perhaps using outline arguments and filling in details if doubt arises (see [Jon96]; Jackson and Wing made a similar point in the same journal; also my position paper at the Royal Society meeting in October 2004 – yet to be printed). But how do we know that the specification is right? This is not a trivial ques-tion especially with the way computers are today. As computers have become more powerful and less expensive, they have become ever more deeply embedded in the way nearly everyone works. In their short history, computers have moved from batch processors in their own buildings to work tools on every desk (or lap)